#include <stdlib.h>
#include "matrice.h"

inline int abs (int x)
{
	/* Plus rapide qu'un 'if'. */
	return (x > 0) ? x : -x;
}

void init_matrice (t_matrice* matrice)
{
	/**
	  * La matrice est initialisée au départ à une taille prédefinie pour éviter
	  * qu'elle soit redimensionnée à chaque ajout. Sa taille n'est réduite à la
	  *taille réelle qu'à la fin du chargement d'un fichier.
	  **/
	matrice->elements = (t_element*) malloc(sizeof(t_element)*TAILLE_MATRICE_INIT);
	matrice->taille = TAILLE_MATRICE_INIT;
	matrice->nb_elements = 0;
	matrice->nb_clauses_a_traiter = 0;
}

void agrandir_matrice (t_matrice* matrice)
{
	int taille = matrice->taille * COEF_AGRANDISSEMENT_MATRICE;
	matrice->elements = (t_element*) realloc((matrice->elements), taille*sizeof(t_element));
	matrice->taille = taille;
}

void reduire (t_matrice* matrice)
{
	matrice->elements = (t_element*) realloc(matrice->elements, sizeof(t_element)*matrice->nb_elements);
	matrice->taille = matrice->nb_elements;
}

void ajouter (t_matrice* matrice,
			  t_clause* tab_clauses,
			  t_litteral* tab_variables,
			  int num_clause,
			  int num_variable
			  )
{
	/* Vérifier si la structure qui contient la matrice ne déborde pas */
	if (matrice->taille <= matrice->nb_elements+1) {
		agrandir_matrice(matrice);
	}

	/* Mettre à jour le pointeur "ptr_clause_suiv" de l'element qui précède */
	if (tab_clauses[num_clause].ptr_premier == NON_SIGNIFICATIF) {
		
		/* La clause est vide, on insère son premier élément */	
		matrice->elements[matrice->nb_elements].ptr_clause_prec = NON_SIGNIFICATIF;
		
		/**
		  * nb_elements contient l'indice de l'élément que nous allons insérer puisque
		  * les cases de la matrice sont indexées à partir de 0...
		  **/
		tab_clauses[num_clause].ptr_premier = matrice->nb_elements;
		
	} else {
		
		/**
		  * La clause n'est pas vide, ajuster les pointeurs de la case qui précéde
		  * (dans le sens de la clause courante)
		  **/
		matrice->elements[matrice->nb_elements].ptr_clause_prec = 
			tab_clauses[num_clause].ptr_dernier;
			
		matrice->elements[tab_clauses[num_clause].ptr_dernier].ptr_clause_suiv = 
			matrice->nb_elements;
	}
	
	/**
	  * Mettre à jour l'indice de l'élément precédent 
	  * (dans le sens de la clause courante)
	  **/
	tab_clauses[num_clause].ptr_dernier = matrice->nb_elements;
	
	/* Ajuster le chaînage dans le sens de la variable courante */
	if (tab_variables[abs(num_variable)].ptr_dernier == NON_SIGNIFICATIF) {
		/* Première occurence de la variable */
		tab_variables[abs(num_variable)].ptr_premier = matrice->nb_elements;
	} else {
		/* Mettre à jour le lien suiv. de la précédente occurence */
		matrice->elements[tab_variables[abs(num_variable)].ptr_dernier].ptr_var_suiv = matrice->nb_elements;
	}
	
	/**
	  * Mettre à jour l'indice de l'élément precédent 
	  * (dans le sens de la variable courante)
	  **/
	tab_variables[abs(num_variable)].ptr_dernier = matrice->nb_elements;
	
	/* Enregistrer l'élément dans la matrice */
	matrice->elements[matrice->nb_elements].num_clause = num_clause;
	matrice->elements[matrice->nb_elements].num_variable = num_variable;
	matrice->elements[matrice->nb_elements].ptr_clause_suiv = NON_SIGNIFICATIF;
	matrice->elements[matrice->nb_elements].ptr_var_suiv = NON_SIGNIFICATIF;
	
	/* Incrémenter les compteurs d'occurences (cf. choisir_variable) */
	if (num_variable >= 0)
	{
		(tab_variables[abs(num_variable)].nb_occ_pos)++;
	} else {
		(tab_variables[abs(num_variable)].nb_occ_neg)++;
	}
	
	/* Incrémenter le nombre d'éléments de la matrice */
	matrice->nb_elements++;	
}

t_clause* init_clauses (int nb_clauses)
{
	/**
	  * La clause 0 servira à stocker le nombre de clauses
	  * dans son pointeur ptr_premier, d'où le +1
	  **/
	t_clause* tab_clauses = malloc((nb_clauses+1) * sizeof(t_clause));
	
	/**
	  * Ajuster le nombre de clauses 
	  */
	tab_clauses[0].ptr_premier = nb_clauses;
	
	for (int i = 1; i < nb_clauses+1; i++){
		tab_clauses[i].etat = INCHANGEE;
		tab_clauses[i].ptr_premier = NON_SIGNIFICATIF;
		tab_clauses[i].ptr_dernier = NON_SIGNIFICATIF;
	 }
	 
	 return tab_clauses;
}

t_litteral* init_variables (int nb_litteraux)
{
	
	/**
	  * La variable 0 servira à stocker le nombre de variables
	  * dans son pointeur ptr_premier, d'où le +1
	  **/
	t_litteral* tab_variables = malloc((nb_litteraux+1) * sizeof(t_litteral));
	tab_variables[0].ptr_premier = nb_litteraux;
	
	/**
	  * L'initialisation à NEUTRE est nécessaire pour pouvoir 
	  * gérer les fichiers où toutes les variables ne sont pas
	  * représentées. Une variable qui reste neutre n'aura pas
	  * d'influence sur le problème (elle restera neutre dans
	  * la solution).
	  */
	for (int i = 1; i < nb_litteraux+1; i++){
		tab_variables[i].etat = NEUTRE;
		tab_variables[i].ptr_premier = NON_SIGNIFICATIF;
		tab_variables[i].ptr_dernier = NON_SIGNIFICATIF;
		tab_variables[i].nb_occ_pos = 0;
		tab_variables[i].nb_occ_neg = 0;
	 }
	 
	 return tab_variables;
}

inline int est_unitaire (t_clause* tab_clauses,
				  int num_clause)
{

	return tab_clauses[num_clause].ptr_premier == 
		   tab_clauses[num_clause].ptr_dernier;
}

inline int est_marque_satisfaite (t_clause* tab_clauses,
				  	 	   int num_clause
				 		  )
{
	return tab_clauses[num_clause].etat == SATISFAITE;
}

inline int nombre_clauses (t_clause* tab_clauses)
{
	/* cf. structure */
	return tab_clauses[0].ptr_premier;
}

inline int nombre_variables (t_litteral* tab_variables)
{
	/* cf. structure */
	return tab_variables[0].ptr_premier;
}

inline int toutes_satisfaites (t_matrice* matrice)
{
	return (matrice->nb_clauses_a_traiter <= 0);
}